Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	0(#)	→ #
2:	x + #	→ x
3:	# + x	→ x
4:	0(x) + 0(y)	→ 0(x + y)
5:	0(x) + 1(y)	→ 1(x + y)
6:	1(x) + 0(y)	→ 1(x + y)
7:	1(x) + 1(y)	→ 0((x + y) + 1(#))
8:	(x + y) + z	→ x + (y + z)
9:	# - x	→ #
10:	x - #	→ x
11:	0(x) - 0(y)	→ 0(x - y)
12:	0(x) - 1(y)	→ 1((x - y) - 1(#))
13:	1(x) - 0(y)	→ 1(x - y)
14:	1(x) - 1(y)	→ 0(x - y)
15:	not(true)	→ false
16:	not(false)	→ true
17:	if(true,x,y)	→ x
18:	if(false,x,y)	→ y
19:	eq(#,#)	→ true
20:	eq(#,1(y))	→ false
21:	eq(1(x),#)	→ false
22:	eq(#,0(y))	→ eq(#,y)
23:	eq(0(x),#)	→ eq(x,#)
24:	eq(1(x),1(y))	→ eq(x,y)
25:	eq(0(x),1(y))	→ false
26:	eq(1(x),0(y))	→ false
27:	eq(0(x),0(y))	→ eq(x,y)
28:	ge(0(x),0(y))	→ ge(x,y)
29:	ge(0(x),1(y))	→ not(ge(y,x))
30:	ge(1(x),0(y))	→ ge(x,y)
31:	ge(1(x),1(y))	→ ge(x,y)
32:	ge(x,#)	→ true
33:	ge(#,0(x))	→ ge(#,x)
34:	ge(#,1(x))	→ false
35:	log(x)	→ log'(x) - 1(#)
36:	log'(#)	→ #
37:	log'(1(x))	→ log'(x) + 1(#)
38:	log'(0(x))	→ if(ge(x,1(#)),log'(x) + 1(#),#)
39:	# * x	→ #
40:	0(x) * y	→ 0(x * y)
41:	1(x) * y	→ 0(x * y) + y
42:	(x * y) * z	→ x * (y * z)
43:	x * (y + z)	→ (x * y) + (x * z)
44:	app(nil,l)	→ l
45:	app(cons(x,l1),l2)	→ cons(x,app(l1,l2))
46:	sum(nil)	→ 0(#)
47:	sum(cons(x,l))	→ x + sum(l)
48:	sum(app(l1,l2))	→ sum(l1) + sum(l2)
49:	prod(nil)	→ 1(#)
50:	prod(cons(x,l))	→ x * prod(l)
51:	prod(app(l1,l2))	→ prod(l1) * prod(l2)
52:	mem(x,nil)	→ false
53:	mem(x,cons(y,l))	→ if(eq(x,y),true,mem(x,l))
54:	inter(x,nil)	→ nil
55:	inter(nil,x)	→ nil
56:	inter(app(l1,l2),l3)	→ app(inter(l1,l3),inter(l2,l3))
57:	inter(l1,app(l2,l3))	→ app(inter(l1,l2),inter(l1,l3))
58:	inter(cons(x,l1),l2)	→ ifinter(mem(x,l2),x,l1,l2)
59:	inter(l1,cons(x,l2))	→ ifinter(mem(x,l1),x,l2,l1)
60:	ifinter(true,x,l1,l2)	→ cons(x,inter(l1,l2))
61:	ifinter(false,x,l1,l2)	→ inter(l1,l2)

There are 71 dependency pairs:


62:	0(x) +# 0(y)	→ 0#(x + y)
63:	0(x) +# 0(y)	→ x +# y
64:	0(x) +# 1(y)	→ x +# y
65:	1(x) +# 0(y)	→ x +# y
66:	1(x) +# 1(y)	→ 0#((x + y) + 1(#))
67:	1(x) +# 1(y)	→ (x + y) +# 1(#)
68:	1(x) +# 1(y)	→ x +# y
69:	(x + y) +# z	→ x +# (y + z)
70:	(x + y) +# z	→ y +# z
71:	0(x) -# 0(y)	→ 0#(x - y)
72:	0(x) -# 0(y)	→ x -# y
73:	0(x) -# 1(y)	→ (x - y) -# 1(#)
74:	0(x) -# 1(y)	→ x -# y
75:	1(x) -# 0(y)	→ x -# y
76:	1(x) -# 1(y)	→ 0#(x - y)
77:	1(x) -# 1(y)	→ x -# y
78:	EQ(#,0(y))	→ EQ(#,y)
79:	EQ(0(x),#)	→ EQ(x,#)
80:	EQ(1(x),1(y))	→ EQ(x,y)
81:	EQ(0(x),0(y))	→ EQ(x,y)
82:	GE(0(x),0(y))	→ GE(x,y)
83:	GE(0(x),1(y))	→ NOT(ge(y,x))
84:	GE(0(x),1(y))	→ GE(y,x)
85:	GE(1(x),0(y))	→ GE(x,y)
86:	GE(1(x),1(y))	→ GE(x,y)
87:	GE(#,0(x))	→ GE(#,x)
88:	LOG(x)	→ log'(x) -# 1(#)
89:	LOG(x)	→ LOG'(x)
90:	LOG'(1(x))	→ log'(x) +# 1(#)
91:	LOG'(1(x))	→ LOG'(x)
92:	LOG'(0(x))	→ IF(ge(x,1(#)),log'(x) + 1(#),#)
93:	LOG'(0(x))	→ GE(x,1(#))
94:	LOG'(0(x))	→ log'(x) +# 1(#)
95:	LOG'(0(x))	→ LOG'(x)
96:	0(x) *# y	→ 0#(x * y)
97:	0(x) *# y	→ x *# y
98:	1(x) *# y	→ 0(x * y) +# y
99:	1(x) *# y	→ 0#(x * y)
100:	1(x) *# y	→ x *# y
101:	(x * y) *# z	→ x # (y z)
102:	(x * y) *# z	→ y *# z
103:	x *# (y + z)	→ (x * y) +# (x * z)
104:	x *# (y + z)	→ x *# y
105:	x *# (y + z)	→ x *# z
106:	APP(cons(x,l1),l2)	→ APP(l1,l2)
107:	SUM(nil)	→ 0#(#)
108:	SUM(cons(x,l))	→ x +# sum(l)
109:	SUM(cons(x,l))	→ SUM(l)
110:	SUM(app(l1,l2))	→ sum(l1) +# sum(l2)
111:	SUM(app(l1,l2))	→ SUM(l1)
112:	SUM(app(l1,l2))	→ SUM(l2)
113:	PROD(cons(x,l))	→ x *# prod(l)
114:	PROD(cons(x,l))	→ PROD(l)
115:	PROD(app(l1,l2))	→ prod(l1) *# prod(l2)
116:	PROD(app(l1,l2))	→ PROD(l1)
117:	PROD(app(l1,l2))	→ PROD(l2)
118:	MEM(x,cons(y,l))	→ IF(eq(x,y),true,mem(x,l))
119:	MEM(x,cons(y,l))	→ EQ(x,y)
120:	MEM(x,cons(y,l))	→ MEM(x,l)
121:	INTER(app(l1,l2),l3)	→ APP(inter(l1,l3),inter(l2,l3))
122:	INTER(app(l1,l2),l3)	→ INTER(l1,l3)
123:	INTER(app(l1,l2),l3)	→ INTER(l2,l3)
124:	INTER(l1,app(l2,l3))	→ APP(inter(l1,l2),inter(l1,l3))
125:	INTER(l1,app(l2,l3))	→ INTER(l1,l2)
126:	INTER(l1,app(l2,l3))	→ INTER(l1,l3)
127:	INTER(cons(x,l1),l2)	→ IFINTER(mem(x,l2),x,l1,l2)
128:	INTER(cons(x,l1),l2)	→ MEM(x,l2)
129:	INTER(l1,cons(x,l2))	→ IFINTER(mem(x,l1),x,l2,l1)
130:	INTER(l1,cons(x,l2))	→ MEM(x,l1)
131:	IFINTER(true,x,l1,l2)	→ INTER(l1,l2)
132:	IFINTER(false,x,l1,l2)	→ INTER(l1,l2)

The approximated dependency graph contains 14 SCCs: {106}, {78}, {79}, {80,81}, {87}, {63-65,67-70}, {97,100-102,104,105}, {114,116,117}, {72-75,77}, {82,84-86}, {120}, {122,123,125-127,129,131,132}, {91,95} and {109,111,112}.

Consider the SCC {106}. There are no usable rules. By taking the AF π with π(APP) = 1 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 106 is strictly decreasing.

Consider the SCC {78}. There are no usable rules. By taking the AF π with π(EQ) = 2 together with the lexicographic path order with empty precedence, rule 78 is strictly decreasing.

Consider the SCC {79}. There are no usable rules. By taking the AF π with π(EQ) = 1 together with the lexicographic path order with empty precedence, rule 79 is strictly decreasing.

Consider the SCC {80,81}. There are no usable rules. By taking the AF π with π(0) = π(EQ) = 1 together with the lexicographic path order with empty precedence, rule 81 is weakly decreasing and rule 80 is strictly decreasing. There is one new SCC.
- Consider the SCC {81}. By taking the AF π with π(EQ) = 1 together with the lexicographic path order with empty precedence, rule 81 is strictly decreasing.

Consider the SCC {87}. There are no usable rules. By taking the AF π with π(GE) = 2 together with the lexicographic path order with empty precedence, rule 87 is strictly decreasing.

Consider the SCC {63-65,67-70}. The usable rules are {1-8}. The constraints could not be solved.

Consider the SCC {97,100-102,104,105}. The usable rules are {1-8,39-43}. The constraints could not be solved.

Consider the SCC {114,116,117}. There are no usable rules. By taking the AF π with π(PROD) = 1 and π(cons) = 2 together with the lexicographic path order with empty precedence, rule 114 is weakly decreasing and the rules in {116,117} are strictly decreasing. There is one new SCC.
- Consider the SCC {114}. By taking the AF π with π(PROD) = 1 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 114 is strictly decreasing.

Consider the SCC {72-75,77}. The usable rules are {1,9-14}. By taking the AF π with π(-) = π(-#) = 1 together with the lexicographic path order with precedence 1 ≈ 0, the rules in {9-14} are weakly decreasing and the rules in {1,72-75,77} are strictly decreasing.

Consider the SCC {82,84-86}. There are no usable rules. The constraints could not be solved.

Consider the SCC {120}. There are no usable rules. By taking the AF π with π(MEM) = 2 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 120 is strictly decreasing.

Consider the SCC {122,123,125-127,129,131,132}. The usable rules are {17-27,52,53}. The constraints could not be solved.

Consider the SCC {91,95}. There are no usable rules. By taking the AF π with π(0) = π(LOG') = 1 together with the lexicographic path order with empty precedence, rule 95 is weakly decreasing and rule 91 is strictly decreasing. There is one new SCC.
- Consider the SCC {95}. By taking the AF π with π(LOG') = 1 together with the lexicographic path order with empty precedence, rule 95 is strictly decreasing.

Consider the SCC {109,111,112}. There are no usable rules. By taking the AF π with π(SUM) = 1 and π(cons) = 2 together with the lexicographic path order with empty precedence, rule 109 is weakly decreasing and the rules in {111,112} are strictly decreasing. There is one new SCC.
- Consider the SCC {109}. By taking the AF π with π(SUM) = 1 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 109 is strictly decreasing.

Tyrolean Termination Tool (24.53 seconds) --- May 4, 2006